/*
 * CSListRepresentation.hpp
 *
 * Copyright 2012 fabian
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#ifndef CSLISTREPRESENTATION_HPP_
#define CSLISTREPRESENTATION_HPP_

#include <list>

#include "bfr/Literal.hpp"
#include "bfr/ClauseSet.hpp"

namespace bfr {

/**
 * The usual representation of DNFs and CNFs is based on sets,
 * this one on lists.
 *
 * Sometimes we don't really need all the functions provided by the
 * ClauseSet class. We just want to store a collection of Clauses.
 * For example this class does not have a contains method.
 * However for some algorithms this representation is better
 * than the set solution.
 *
 * This implementation for example does not care about multiple occurrences
 * of objects.
 *
 * The implementation is based on <code>std::lists</code>s.
 *
 */
class CSListRepresentation {

    public:
        /**
         * Type of the clauses (list of Literal).
         */
        typedef std::list<Literal> clause_t;

        /**
         * Type of the content (list of list of Literal).
         */
        typedef std::list<clause_t> content_t;

        /**
         * Const iterator type.
         */
        typedef content_t::const_iterator const_iterator;

        /**
         * Constructor that creates an empty list.
         */
        CSListRepresentation();

        /**
         * Constructs a new list with the content of the clause set.
         *
         * @param cs The clause set.
         */
        CSListRepresentation(const ClauseSet &cs);

        /**
         * Add a clause to the list.
         *
         * @param clause The clause to add.
         */
        void addClause(const clause_t &clause);

        /**
         * Return an iterator to the beginning.
         */
        const_iterator begin() const;

        /**
         * Return an iterator to the end.
         */
        const_iterator end() const;

    private:
        content_t content;

};

}

#endif  // CSLISTREPRESENTATION_HPP_
